$\forall$${\it the\_es}$:event\_system\{i:l\}, $l$:IdLnk, $e$:es{-}E(${\it the\_es}$).
\\[0ex]es{-}sends(${\it the\_es}$; $l$; $e$) $\in$ (es{-}Msgl(${\it the\_es}$; $l$) List)